$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type. $\forall$$x$$\in$dom(${\it ds}$). $A$=${\it ds}$($x$) $\Rightarrow$  $A$ $\Rightarrow$ Normal(${\it ds}$)